Product Code Database
In computer science, formal methods are mathematics rigorous techniques for the specification, development, Program analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, , automata theory, control theory, program semantics, type systems, and type theory.Monin, pp.3-4
Alternatively, specification may be the only stage in which formal methods is used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.
The need for formal specification systems has been noted for years. In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus–Naur form (BNF).Donald Knuth (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736. Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.
Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification, and by inference, properties of the system implementation.
Critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.
Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.
Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.
Critics note that some of those systems are like Oracle machine: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.
The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operatorsA. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, (2011). to get fast convergence.
There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System, Unmanned Aircraft System integration in National Airspace System,Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE. and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ B-Method with Atelier B, is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.
Formal verification has been frequently used in hardware by most of the well-known hardware vendors, such as IBM, Intel, and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache-coherent protocol,C. T. Chou, P. K. Mannava, S. Park, " A simple method for parameterized verification of cache coherence protocols", Formal Methods in Computer-Aided Design, pp. 382–398, 2004. Intel Core i7 processor execution engine validation Formal Verification in Intel Core i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 , accessed at September 13, 2013. (using theorem proving, BDDs, and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,J. Grundy, "Verified optimizations for the Intel IA-64 architecture", In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232. and verification of high-performance dual-port gigabit Ethernet controller with support for PCI Express protocol and Intel advance management technology using Cadence.E. Seligman, I. Yarom, " Best known methods for using Cadence Conformal LEC", at Intel. Similarly, IBM has used formal methods in the verification of power gates,C. Eisner, A. Nahir, K. Yorav, "ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449", Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445. registers,P. C. Attie, H. Chockler, " Automatic verification of fault-tolerant register emulations", Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60. and functional verification of the IBM Power7 microprocessor.K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, " Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems", IBM Journal of Research and Development, vol. 55, no 3.
For sequential software, examples of formal methods include the B-Method, the specification languages used in automated theorem proving, RAISE, and the Z notation.
In functional programming, QuickCheck has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions.
The Object Constraint Language (and specializations such as Java Modeling Language) has allowed object-oriented systems to be formally specified, if not necessarily formally verified.
For concurrent software and systems, , process algebra, and finite-state machines (which are based on automata theory; see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behaviour.
Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of first-order logic—and then to directly execute the logic as though it were a program. The OWL language, based on description logic, is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are Attempto Controlled English, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.
Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" , Crosstalk: The Journal of Defense Software Engineering, January 2003 They contend that the expressiveness of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various lightweight formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the Alloy language object modelling notation,Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290 Denney's synthesis of some aspects of the Z notation with use case driven development,Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, . and the CSK VDM Tools.Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" , In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
|
|
